(declare-const x Float32)
(declare-const y Float32)
(declare-const z Float32)
(declare-const r Float32)
(declare-const w Float32)
(assert (= x (fp #b0 #b01111111 #b00000000101111111111111)))
(assert (= y (fp #b0 #b01111111 #b00000001001110001010111)))
(assert (= z (fp #b1 #b01111111 #b00000001111110011001011)))
(assert (= r (fp #b0 #b01100110 #b00000000000111010100100)))
(assert (= w (fp.fma RNE x y z)))
(assert (not (= w r)))
(check-sat)
